/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.ast;


import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.JoinableList;
import static edu.ut.ece382c.valloy.ast.Type.EMPTY;

/**
 * Immutable; represents a unary expression of the form "(OP subexpression)"
 *
 * <p> <b>Invariant:</b>  type!=EMPTY => sub.mult==0
 */

public final class ExprUnary extends Expr {

    /** The unary operator. */
    public final Op op;

    /** The subexpression. */
    public final Expr sub;

    /** Caches the span() result. */
    private Pos span=null;

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public Pos span() {
        Pos p=span;
        if (p==null) { if (op==Op.NOOP && pos!=Pos.UNKNOWN) span=(p=pos); else span=(p=pos.merge(sub.span())); }
        return p;
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent, boolean newline) {

    	for(int i=0; i<indent && newline; i++) { out.append(' '); }
    	switch(op) {
    		case SOMEOF: 		out.append("some "); break;
    		case LONEOF:	 	out.append("lone "); break;
    		case ONEOF: 		out.append("one "); break;
    		case SETOF: 		out.append("set "); break;
    		case NO:			// fall-thru
    		case SOME:			// fall-thru
    		case LONE:			// fall-thru
    		case ONE: 			out.append(op + " "); break;
    		case CAST2INT: 		out.append("int["); sub.toString(out,indent, false); out.append(']'); return;
    		case CAST2SIGINT: 	out.append("Int["); sub.toString(out,indent, false); out.append(']'); return;
    		case NOOP: 			break;
    		default: 			out.append(op);
    	}
    	out.append('(');
    	sub.toString(out, indent, false);
    	out.append(')');
    }

    //============================================================================================================//

    /** Constructs an unary expression. */
    private ExprUnary(Pos pos, Op op, Expr sub, Type type, long weight, JoinableList<Err> errors) {
        super(pos, null, sub.ambiguous, type, (op==Op.SOMEOF||op==Op.LONEOF||op==Op.ONEOF||op==Op.SETOF)?1:0, weight, errors);
        this.op = op;
        this.sub = sub;
    }

    //============================================================================================================//

    /** This class contains all possible unary operators. */
    public enum Op {
        /** :some x (where x is a unary set)                             */  SOMEOF("some of"),
        /** :lone x (where x is a unary set)                             */  LONEOF("lone of"),
        /** :one  x (where x is a unary set)                             */  ONEOF("one of"),
        /** :set  x (where x is a set or relation)                       */  SETOF("set of"),
        /** not   f (where f is a formula)                               */  NOT("!"),
        /** no    x (where x is a set or relation)                       */  NO("no"),
        /** some  x (where x is a set or relation)                       */  SOME("some"),
        /** lone  x (where x is a set or relation)                       */  LONE("lone"),
        /** one   x (where x is a set or relation)                       */  ONE("one"),
        /** transpose                                                    */  TRANSPOSE("~"),
        /** reflexive closure                                            */  RCLOSURE("*"),
        /** closure                                                      */  CLOSURE("^"),
        /** cardinality of x (truncated to the current integer bitwidth) */  CARDINALITY("#"),
        /** IntAtom-to-integer                                           */  CAST2INT("Int->int"),
        /** integer-to-IntAtom                                           */  CAST2SIGINT("int->Int"),
        /** No-Operation                                                 */  NOOP("NOOP");

        /** The constructor */
        private Op(String label) {this.label=label;}

        /** The human readable label for this operator */
        private final String label;

        /**
         * Construct an ExprUnary node.
         * @param pos - the original position of the "unary operator" in the file (can be null if unknown)
         * @param sub - the subexpression
         *
         * <p>  Alloy4 disallows multiplicity like this:   "variable : one (X lone-> Y)",
         * <br> that is, a some/lone/one in front of an arrow multiplicity declaration.
         * <br> Alloy4 does allow "variable : set (X lone-> Y)", where we ignore the word "set".
         * <br> (This desugaring is done by the ExprUnary.Op.make() method, so ExprUnary's constructor never sees it)
         */
        public final Expr make(Pos pos, Expr sub) { return make(pos, sub, null, 0); }

        /**
         * Construct an ExprUnary node.
         * @param pos - the original position of the "unary operator" in the file (can be null if unknown)
         * @param sub - the subexpression
         * @param extraError - if nonnull, it will be appended as an extra error
         * @param extraWeight - it's the amount of extra weight
         *
         * <p>  Alloy4 disallows multiplicity like this:   "variable : one (X lone-> Y)",
         * <br> that is, a some/lone/one in front of an arrow multiplicity declaration.
         * <br> Alloy4 does allow "variable : set (X lone-> Y)", where we ignore the word "set".
         * <br> (This desugaring is done by the ExprUnary.Op.make() method, so ExprUnary's constructor never sees it)
         */
        public final Expr make(Pos pos, Expr sub, Err extraError, long extraWeight) {
        	return new ExprUnary(pos, this, sub, EMPTY, extraWeight + sub.weight, null);
        }

        /** Returns the human readable label for this operator */
        @Override public final String toString() { return label; }
    }

    //============================================================================================================//

    /** {@inheritDoc} */
    public int getDepth() { return 1 + sub.getDepth(); }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }
}
